$\forall$${\it es}$:ES, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $i$:Id.
\\[0ex]($\forall$$x$:Id. vartype($i$;$x$) $\subseteq\rho$ ${\it ds}$($x$)?Top)
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. loc($e$) $=$ $i$ $\Rightarrow$ valtype($e$) $\subseteq\rho$ ${\it da}$(kind($e$))?Top)
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. loc($e$) $=$ $i$ $\Rightarrow$ es{-}info(${\it es}$;$e$) $\in$ event{-}info(${\it ds}$;${\it da}$))